T913: cid + not discrete => uncountable pi-character#1813
Conversation
ouch
|
| and let $\mathscr V$ be a countable collection of nonempty open sets. | ||
| To show $X$ has uncountable $\pi$-character, we show that $\mathscr V$ is not a local $\pi$-base for $x$. | ||
| Each $V\in\mathscr V$ contains a point $x_V\ne x$. | ||
| The set $F:=\{x_V:V\in\mathscr V\}$ is countable, hence closed since $X$ is {P168}. |
There was a problem hiding this comment.
For this to make sense you have to click on P168. When I read it I was breifly confused.
Maybe you can write "(see [the stackexchange post we use in P168)", to make this clearer?
There was a problem hiding this comment.
Equivalent conditions for P168:
- every countable set is closed.
- every countable set is discrete.
When P168 was first introduced, it was called countable sets are closed, as it seemed useful but we did not know it had appeared in the literature. Later on, we learned that it was equivalent to countable sets are discrete, sometimes called "cid" in the literature. So we changed the main name to that discrete version.
The problem is that previous proof justifications from before the name change became hard to understand because {P168} now expands to something seemingly unrelated. These proofs should be updated. e.g. https://topology.pi-base.org/theorems/T000417.
For this PR I prefer not to refer to the mathse post here, but I'll rephrase things.
(This comes from the list of Theorems.) @StevenClontz is that something that could be fixed in pi-data/web? |
In fact this appears earlier lot of times, e.g., T88. |
|
Thanks @yhx-12243. I think if something could be done to improve the layout of the expanded text, that would be good. Low priority of course. Let's see what @StevenClontz thinks. |
3 participants
New T913:
cid + ~ discrete => ~ countable pi-characterThis allows to derive that 8 more spaces have uncountable pi-character:
π-Base, Search for
cid + ~ discrete + ? Has countable $\pi$-character